0.00/0.33	YES
0.00/0.33	
0.00/0.33	Problem:
0.00/0.33	 app (abs (\x. F x)) S -> F S
0.00/0.33	 abs (\x. app S x) -> S
0.00/0.33	
0.00/0.33	Proof:
0.00/0.33	 Higher-Order Church Rosser Processor:
0.00/0.33	  app (abs (\x. F x)) S -> F S
0.00/0.33	  abs (\x. app S x) -> S
0.00/0.33	  critical peaks: 2
0.00/0.33	   abs (\14. 12 14) <-[1,0]-> abs (\11. 12 11)
0.00/0.33	   app 24 S <-[0,1]-> app 24 S
0.00/0.33	   
0.00/0.33	   Higher-Order Closedness Processor:
0.00/0.33	     all critical pairs are trivial
0.00/0.33	    
0.00/0.33	    Qed
0.00/0.33	 
0.00/0.33	EOF